
import junit.framework.Assert;
import nz.ac.waikato.modeljunit.Action;
import nz.ac.waikato.modeljunit.FsmModel;
import nz.ac.waikato.modeljunit.GreedyTester;
import nz.ac.waikato.modeljunit.Tester;
import nz.ac.waikato.modeljunit.VerboseListener;
import nz.ac.waikato.modeljunit.coverage.TransitionCoverage;
import nz.ac.waikato.modeljunit.coverage.TransitionPairCoverage;

public class CalcEFSMAdaptor implements FsmModel{
	
	public enum State{
		Initial,
		Parentheses,
		Digit,
		Number,
		Operation,
		Result,
	};
	
	private State currState;
	private int pc;
	private Boolean buffer;
	private Boolean operand;
	private Boolean operation;
	private Calculator3 sut; 
	
	public CalcEFSMAdaptor(){
		sut = new Calculator3();
		currState = State.Initial;
		pc = 0;
		buffer = false;
		operand =false;
		operation = false;
	}
	
	public CalcEFSMAdaptor(Calculator3 sut){
		this.sut = sut;
	}
	
	@Override
	public Object getState() {
		return currState.toString();
	}

	@Override
	public void reset(boolean arg0) {
		currState = State.Initial;
		pc = 0;
		buffer = false;
		operand =false;
		operation = false;
	}
	
	/*
	 * Press Open Bracket Guard
	 * Open bracket only allowed in the states Parentheses,
	 * Initial and Operation.
	 * 
	 */
	public boolean oBracketGuard(){
		return currState == State.Initial || 
			   currState == State.Parentheses ||
			   currState == State.Operation;
	}
	
	/*
	 * Press Open Bracket
	 */
	@Action
	public void oBracket(){
		pc++;
		currState=State.Parentheses;
		sut.pressOpenBracket();
		checkSUT();
	}
	
	/*
	 * 
	 */
	public boolean pressOneGuard(){
		return currState == State.Initial ||
			   currState == State.Parentheses ||
			   currState == State.Digit ||
			   currState == State.Operation;
	}
	/*
	 * Press the digit one
	 */
	@Action
	public void pressOne(){
		if(currState==State.Operation)
		{
			this.buffer=false;
		}
		
		buffer = true;
		currState=State.Digit;
		
		sut.pressDigit('1');
		checkSUT();
		
	}
	
	/*
	 * Guard for press close bracket
	 */
	public boolean cBracketGuard(){
		return ((currState == State.Digit || currState == State.Number) && (pc > 0)) ;
	}
	
	
	/*
	 * Press close bracket
	 */
	@Action
	public void cBracket(){
		pc--;
		currState=State.Number;
		sut.pressCloseBracket();
		checkSUT();
	}
	
	/*
	 * Press Equal Guard
	 */
	public boolean pequalGuard(){
		return (currState==State.Digit||
				currState==State.Number)&& pc==0;
	}
	/*
	 * Press Equal =
	 */
	@Action
	public void pequal(){
		pequalIn();
		currState = State.Result;
		checkSUT();
	}
	
	public void pequalIn(){
		//buffer should contain the result
		buffer = true;
		//operand should be empty
		operand = false;
		//operation should be empty
		operation = false;
		
		sut.pressEqual();
		
		
	}
	
	public boolean pressPlusGuard(){
		return currState == State.Operation ||
				currState == State.Digit ||
				currState == State.Number;
	}
	
	@Action
	public void pressPlus(){
		if(this.operation==false && operand==true)
		{
			this.pequalIn();			
		}
		
		this.operation=true;
		this.operand=true;
		currState=State.Operation;
		
		sut.pressPlus();
		
		checkSUT();
	} 
	
	public void checkSUT(){
		Boolean bufferActual = !sut.getBuffer().isEmpty();
		Boolean operandActual = operandActualCalc();
		Boolean inBracketExpected = bracketExpectedCalc();
		Boolean inBracketActual = sut.CheckInBracket();
		
		Assert.assertEquals("Check buffer", this.buffer, bufferActual);
		Assert.assertEquals("Check operand", this.operand, operandActual);
		Assert.assertEquals("Check brackets", inBracketExpected, inBracketActual);

	}
	
	private Boolean bracketExpectedCalc(){
		return (pc > 0 ? true : false);
	}
	
	private Boolean operandActualCalc(){
		int operandVal = sut.getOperand();
		String bufferVal = sut.getBuffer();
		if(operandVal == 0 && bufferVal.isEmpty()){
			return false;
		}else{
			return true;
		}
	}
	
		
	  /** An example of generating tests from this model. */
	public static void main(String[] args)
	{
	    Calculator3 sut = new Calculator3();
	    Tester tester = new GreedyTester(new CalcEFSMAdaptor());
	  //  Tester tester = new LookaheadTester(new CalcEFSMAdaptor());
	 //   Tester tester = new AllRoundTester(new CalcEFSMAdaptor());
	    tester.buildGraph(); // to get better statistics
	    tester.addListener(new VerboseListener());
	    
	    // uncomment this line if you want to stop when the first error is found.
	    // tester.addListener(new StopOnFailureListener());
	    
	    tester.addCoverageMetric(new TransitionPairCoverage());
	    tester.addCoverageMetric(new TransitionCoverage());
	    tester.generate(5000);
	    tester.printCoverage();
	}
	
	
	
}
